Conversation
When `proc change` bound new local variables, both generated subgoals were ill-formed: the local-equivalence goal carried the fresh local in the memtype of the original (un-replaced) fragment, and the continuation goal rewrote the side to a statement using the fresh local while keeping the un-extended memtype, leaving a program that referenced a variable absent from its memory type. Thread the extended memtype to the side that runs the replacement: in the local-equivalence goal it goes on the right (the new fragment) while the left keeps the original memtype; in the continuation goal it goes on the rewritten side. `hl_set_stmt` gains an optional `?mt` to override the active side's memtype.
fdupress
approved these changes
Jun 10, 2026
fdupress
left a comment
fdupress
left a comment
Member
There was a problem hiding this comment.
Should we add unit tests for the memtype-changing variants of proc change?
This does fix the problem also in the context of my broader proof, so the fix is verified for me.
Member
Author
I don't know how to add a test that would capture this. In fact, this will be caught one we recheck the goals that we push in an environment. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #1026.
When
proc changebound new local variables, both generated subgoalswere ill-formed: the local-equivalence goal carried the fresh local in
the memtype of the original (un-replaced) fragment, and the continuation
goal rewrote the side to a statement using the fresh local while keeping
the un-extended memtype, leaving a program that referenced a variable
absent from its memory type.
Thread the extended memtype to the side that runs the replacement: in
the local-equivalence goal it goes on the right (the new fragment) while
the left keeps the original memtype; in the continuation goal it goes on
the rewritten side.
hl_set_stmtgains an optional?mtto override theactive side's memtype.